Nuprl Lemma : fpf-ap-compose
11,40
postcript
pdf
x
:Top,
f
:
a
:Top fp
Top,
g
,
eq
:Top.
g
o
f
(
x
) ~ (
g
(
f
(
x
)))
latex
Definitions
Top
,
t
T
,
x
.
t
(
x
)
,
x
:
A
.
B
(
x
)
,
a
:
A
fp
B
(
a
)
,
fpf
ap
compose
compseq
tag
def
Lemmas
fpf
wf
,
top
wf
origin
x:Top, f:a:Top fp
Top, g, eq:Top. g o f(x) ~ (g(f(x))) x:Top, f:a:Top fp Top, g, eq:Top. g o f(x) ~ (g(f(x))) 
T
x. t(x)x:A. B(x) B(a)